﻿using System;
using System.Collections.Generic;
using System.Collections;
using System.Text;

namespace mi2project{

    //a lényeg lent van    

    class Helyettesítés
    {
        public Parameter mit;
        public Parameter mire;
        public Helyettesítés(Parameter Mit, Parameter Mire)
        {
            mit = new Parameter(Mit);
            mire = new Parameter(Mire);
        }       

    }
          

    class Változóhelyettesítés{

        //ez kell a stringtoaxioma miatt

        public List<string> konstansok = new List<string>();



        public Változóhelyettesítés(List<string> konst)
        {
            konstansok = new List<string>(konst);
        }



        public Axioma HelyettesítéstVégrehajt(Axioma Ax, List<Helyettesítés> eh)
        {
            Axioma ax = new Axioma(Ax);

            for (int i = 0; i < eh.Count; ++i)
            {
                List<Parameter> par = ax.getParameterek();
                for (int j = 0; j < par.Count; ++j)
                {
                    if (par[j].tipus == "f")
                    {
                        Axioma axi = HelyettesítéstVégrehajt(Konzol.StringToAxioma(par[j].nev,konstansok), eh);
                        par[j] = new Parameter(axi.axiomaNezete(), "f");
                        continue;
                    }


                    if (par[j].nev == eh[i].mit.nev && par[j].tipus == eh[i].mit.tipus)
                    {
                        par[j] = eh[i].mire;
                    }
                }

                ax.ParametereketNullaz();


                for (int j = 0; j < par.Count; ++j)
                {
                    ax.parameterekhezAd(par[j]);
                }
            }
            return ax;
        }


        public List<List<Helyettesítés>> HelyettesítéseketÖsszerak(List<List<Helyettesítés>> ret, List<List<Helyettesítés>> eh)
        {            
            List<List<Helyettesítés>> ret2 = new List<List<Helyettesítés>>();
            if (eh.Count == 0 && ret.Count == 0) 
                return ret2;
            if (eh.Count == 0)
            {                                
                ret2.AddRange(ret);
                return ret2;
            }
            if (ret.Count == 0)
            {
                for (int j = 0; j < eh.Count; ++j)
                {
                    ret.Add(new List<Helyettesítés>());
                    ret[j].AddRange(eh[j]);
                }
            }
            else
            {
                int db = ret.Count;
                for (int j = 0; j < eh.Count; ++j)
                {

                    for (int k = j * db; k < db + j * db; ++k)
                    {
                        if (k >= db)
                        {
                            ret.Add(new List<Helyettesítés>(ret[k % db]));
                        }


                    }

                }
                for (int j = 0; j < eh.Count; ++j)
                {

                    for (int k = j * db; k < db + j * db; ++k)
                    {
                        for (int l = 0; l < eh[j].Count; ++l)
                        {
                            ret[k].Add(new Helyettesítés(eh[j][l].mit, eh[j][l].mire));
                        }
                    }

                }
            }
            
            ret2.AddRange(ret);
            return ret2;
        }

        private List<List<Helyettesítés>> EgyesítőHelyettesítések(Axioma ax1, Axioma ax2, int honnan)
        {

            List<List<Helyettesítés>> ret = new List<List<Helyettesítés>>();
            if (ax1.getLiteralok()[0].getParameterekSzama() != ax2.getLiteralok()[0].getParameterekSzama() || honnan >= ax1.getLiteralok()[0].getParameterekSzama() || ax1.getLiteralok().Count != 1 || ax2.getLiteralok().Count != 1)
            {
                return ret;
            }
            List<Parameter> par1, par2;
            par1 = ax1.getParameterek();
            par2 = ax2.getParameterek();
            List<List<Helyettesítés>> temp;
            for (int i = honnan; i < par1.Count; ++i)
            {
                if (par1[i].tipus == "v")
                {
                    if (par2[i].tipus == "v")
                    {
                        if (par1[i].nev == par2[i].nev) continue;


                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());                        
                        temp[0].Add(new Helyettesítés(par1[i], par2[i]));
                        
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));

                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].Add(new Helyettesítés(par2[i], par1[i]));                        
                        temp = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                        ret.AddRange(temp);
                        return ret;                         

                    }
                    if (par2[i].tipus == "k")
                    {
                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].Add(new Helyettesítés(par1[i], par2[i]));
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                        return ret;
                
                    }
                    if (par2[i].tipus == "f")
                    {
                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].Add(new Helyettesítés(par1[i], par2[i]));
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                        return ret;                       
                    }                      
                }
                if (par1[i].tipus == "k")
                {
                    if (par2[i].tipus == "v")
                    {

                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].Add(new Helyettesítés(par2[i], par1[i]));
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                        return ret;                 
                    }
                    if (par2[i].tipus == "k")
                    {
                        if (par1[i].nev != par2[i].nev)
                        {
                            ret = new List<List<Helyettesítés>>();
                            return ret;
                        }
                    }
                    if (par2[i].tipus == "f")
                    {
                        ret = new List<List<Helyettesítés>>();
                        return ret;
                    }
                }
                if (par1[i].tipus == "f")
                {
                    if (par2[i].tipus == "v")
                    {
                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].Add(new Helyettesítés(par2[i], par1[i]));
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                        return ret;                        
                    }
                    if (par2[i].tipus == "k")
                    {
                        ret = new List<List<Helyettesítés>>();
                        return ret;                        
                    }
                    if (par2[i].tipus == "f")
                    {
                        List<List<Helyettesítés>> eh = EgyesítőHelyettesítések(Konzol.StringToAxioma(par1[i].nev,konstansok), Konzol.StringToAxioma(par2[i].nev,konstansok), 0);               

                        
                        if (eh.Count == 0)
                        {
                            ret = new List<List<Helyettesítés>>();
                            return ret;
                        }

                        temp = new List<List<Helyettesítés>>();
                        temp.Add(new List<Helyettesítés>());
                        temp[0].AddRange(eh[0]);
                        ret = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));


                        for (int j = 1; j < eh.Count; ++j)
                        {
                            temp = new List<List<Helyettesítés>>();
                            temp.Add(new List<Helyettesítés>());
                            temp[0].AddRange(eh[j]);
                            temp = HelyettesítéseketÖsszerak(temp, EgyesítőHelyettesítések(HelyettesítéstVégrehajt(ax1, temp[0]), HelyettesítéstVégrehajt(ax2, temp[0]), i + 1));
                            ret.AddRange(temp);
                        }
                        return ret;
                    }
                }
            }

            return ret;
            
        }

        //Megadja az összes lehetséges helyes egyesítő helyettesítését ax1, és ax2-nek
        //ax1 ax2 -ről felteszem, hogy literál ... azért, mert szabályillesztésnél mindig csak 1 literál van.
        // az üres lista azt is jelentheti, hogy nincs helyettesítésük, meg azt is, hogy már egyenlőek.

        public List<List<Helyettesítés>> HelyesEgyesítések(Axioma ax1, Axioma ax2)
        {
            List<List<Helyettesítés>> ret = new List<List<Helyettesítés>>();
            ret.AddRange(EgyesítőHelyettesítések(ax1, ax2, 0));
            Axioma a1;
            Axioma a2;
            a1 = new Axioma();
            a2 = new Axioma();
            for (int i = ret.Count - 1; i >= 0; --i)
            {
                a1 = HelyettesítéstVégrehajt(ax1, ret[i]);
                a2 = HelyettesítéstVégrehajt(ax2, ret[i]);
                if (!Axioma.Egyenlo(a1, a2))
                {
                    ret.RemoveAt(i);
                }
            }
            return ret;
        }
        
    }
}